'Weak Dependency Graph [60.0]'
------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
Details:
We have computed the following set of weak (innermost) dependency pairs:
{ a^#(s(x1)) -> c_0(p^#(s(b(p(p(s(s(x1))))))))
, b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, c^#(s(x1)) -> c_2(p^#(s(p(s(a(p(s(p(s(x1))))))))))
, p^#(p(s(x1))) -> c_3(p^#(x1))
, p^#(s(x1)) -> c_4()}
The usable rules are:
{ a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
The estimated dependency graph contains the following edges:
{a^#(s(x1)) -> c_0(p^#(s(b(p(p(s(s(x1))))))))}
==> {p^#(s(x1)) -> c_4()}
{b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))}
==> {p^#(p(s(x1))) -> c_3(p^#(x1))}
{b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))}
==> {p^#(s(x1)) -> c_4()}
{c^#(s(x1)) -> c_2(p^#(s(p(s(a(p(s(p(s(x1))))))))))}
==> {p^#(s(x1)) -> c_4()}
{p^#(p(s(x1))) -> c_3(p^#(x1))}
==> {p^#(s(x1)) -> c_4()}
{p^#(p(s(x1))) -> c_3(p^#(x1))}
==> {p^#(p(s(x1))) -> c_3(p^#(x1))}
We consider the following path(s):
1) { b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, p^#(p(s(x1))) -> c_3(p^#(x1))
, p^#(s(x1)) -> c_4()}
The usable rules for this path are the following:
{ c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, p^#(p(s(x1))) -> c_3(p^#(x1))
, b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, p^#(s(x1)) -> c_4()}
Details:
We apply the weight gap principle, strictly orienting the rules
{ c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p^#(s(x1)) -> c_4()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p^#(s(x1)) -> c_4()}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [1]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
b^#(x1) = [1] x1 + [1]
c_1(x1) = [1] x1 + [1]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
and weakly orienting the rules
{ c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p^#(s(x1)) -> c_4()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [1]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [5]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
b^#(x1) = [1] x1 + [1]
c_1(x1) = [1] x1 + [1]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))}
and weakly orienting the rules
{ a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p^#(s(x1)) -> c_4()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [4]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [8]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [3]
b^#(x1) = [1] x1 + [13]
c_1(x1) = [1] x1 + [1]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
and weakly orienting the rules
{ b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p^#(s(x1)) -> c_4()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [8]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [12]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [1] x1 + [15]
c_1(x1) = [1] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p^#(p(s(x1))) -> c_3(p^#(x1))}
and weakly orienting the rules
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p^#(s(x1)) -> c_4()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p^#(p(s(x1))) -> c_3(p^#(x1))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [4]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [8]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [3]
b^#(x1) = [1] x1 + [15]
c_1(x1) = [1] x1 + [1]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))}
Weak Rules:
{ p^#(p(s(x1))) -> c_3(p^#(x1))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p^#(s(x1)) -> c_4()}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))}
Weak Rules:
{ p^#(p(s(x1))) -> c_3(p^#(x1))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p^#(s(x1)) -> c_4()}
Details:
The problem is Match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ a_0(8) -> 7
, a_0(8) -> 13
, a_0(8) -> 15
, a_1(29) -> 7
, a_1(29) -> 24
, a_1(29) -> 28
, a_1(29) -> 43
, a_1(29) -> 45
, s_0(2) -> 2
, s_0(2) -> 8
, s_0(2) -> 10
, s_0(2) -> 21
, s_0(2) -> 29
, s_0(2) -> 31
, s_0(2) -> 39
, s_0(6) -> 5
, s_0(7) -> 4
, s_0(7) -> 6
, s_0(10) -> 9
, s_0(13) -> 12
, s_0(15) -> 14
, s_0(16) -> 7
, s_0(16) -> 13
, s_0(16) -> 15
, s_0(17) -> 16
, s_0(18) -> 17
, s_0(20) -> 19
, s_1(2) -> 32
, s_1(2) -> 40
, s_1(22) -> 18
, s_1(22) -> 20
, s_1(22) -> 36
, s_1(22) -> 38
, s_1(23) -> 22
, s_1(24) -> 23
, s_1(27) -> 26
, s_1(28) -> 25
, s_1(28) -> 27
, s_1(31) -> 30
, s_1(32) -> 41
, s_1(34) -> 7
, s_1(34) -> 13
, s_1(34) -> 15
, s_1(34) -> 24
, s_1(34) -> 28
, s_1(34) -> 43
, s_1(34) -> 45
, s_1(35) -> 34
, s_1(36) -> 35
, s_1(38) -> 37
, s_1(43) -> 42
, s_1(45) -> 44
, p_0(2) -> 8
, p_0(2) -> 10
, p_0(2) -> 21
, p_0(5) -> 4
, p_0(9) -> 8
, p_0(10) -> 21
, p_0(12) -> 7
, p_0(14) -> 7
, p_0(14) -> 13
, p_0(19) -> 18
, p_1(25) -> 24
, p_1(26) -> 25
, p_1(27) -> 24
, p_1(30) -> 29
, p_1(32) -> 29
, p_1(32) -> 31
, p_1(32) -> 39
, p_1(37) -> 36
, p_1(40) -> 39
, p_1(41) -> 40
, p_1(42) -> 7
, p_1(42) -> 24
, p_1(42) -> 28
, p_1(44) -> 7
, p_1(44) -> 24
, p_1(44) -> 28
, p_1(44) -> 43
, b_0(21) -> 18
, b_0(21) -> 20
, b_1(39) -> 36
, b_1(39) -> 38
, c_0(8) -> 7
, c_1(29) -> 24
, c_1(29) -> 28
, p^#_0(2) -> 1
, p^#_0(4) -> 3
, p^#_0(6) -> 11
, p^#_1(25) -> 33
, p^#_1(27) -> 46
, b^#_0(2) -> 1
, c_1_0(3) -> 1
, c_1_1(33) -> 1
, c_3_0(11) -> 3
, c_3_1(46) -> 33
, c_4_0() -> 1
, c_4_0() -> 3
, c_4_0() -> 11
, c_4_1() -> 33
, c_4_1() -> 46}
2) { b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, p^#(s(x1)) -> c_4()}
The usable rules for this path are the following:
{ c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, p^#(s(x1)) -> c_4()}
Details:
We apply the weight gap principle, strictly orienting the rules
{c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [1]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [1] x1 + [1]
c_1(x1) = [1] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
and weakly orienting the rules
{c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [1]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [5]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [1] x1 + [1]
c_1(x1) = [1] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p^#(s(x1)) -> c_4()}
and weakly orienting the rules
{ a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p^#(s(x1)) -> c_4()}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [2]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [2]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [8]
b^#(x1) = [1] x1 + [1]
c_1(x1) = [1] x1 + [1]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))}
and weakly orienting the rules
{ p^#(s(x1)) -> c_4()
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [2]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [3]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [1] x1 + [9]
c_1(x1) = [1] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
and weakly orienting the rules
{ b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, p^#(s(x1)) -> c_4()
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [7]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [4]
c(x1) = [1] x1 + [12]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [1] x1 + [15]
c_1(x1) = [1] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, p^#(s(x1)) -> c_4()
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, p^#(s(x1)) -> c_4()
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
Details:
The problem is Match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ a_0(15) -> 14
, a_0(15) -> 19
, a_0(15) -> 21
, a_1(35) -> 14
, a_1(35) -> 30
, a_1(35) -> 34
, a_1(35) -> 49
, a_1(35) -> 51
, s_0(2) -> 2
, s_0(2) -> 15
, s_0(2) -> 17
, s_0(2) -> 27
, s_0(2) -> 35
, s_0(2) -> 37
, s_0(2) -> 45
, s_0(13) -> 12
, s_0(14) -> 11
, s_0(14) -> 13
, s_0(17) -> 16
, s_0(19) -> 18
, s_0(21) -> 20
, s_0(22) -> 14
, s_0(22) -> 19
, s_0(22) -> 21
, s_0(23) -> 22
, s_0(24) -> 23
, s_0(26) -> 25
, s_1(2) -> 38
, s_1(2) -> 46
, s_1(28) -> 24
, s_1(28) -> 26
, s_1(28) -> 42
, s_1(28) -> 44
, s_1(29) -> 28
, s_1(30) -> 29
, s_1(33) -> 32
, s_1(34) -> 31
, s_1(34) -> 33
, s_1(37) -> 36
, s_1(38) -> 47
, s_1(40) -> 14
, s_1(40) -> 19
, s_1(40) -> 21
, s_1(40) -> 30
, s_1(40) -> 34
, s_1(40) -> 49
, s_1(40) -> 51
, s_1(41) -> 40
, s_1(42) -> 41
, s_1(44) -> 43
, s_1(49) -> 48
, s_1(51) -> 50
, p_0(2) -> 15
, p_0(2) -> 17
, p_0(2) -> 27
, p_0(12) -> 11
, p_0(16) -> 15
, p_0(17) -> 27
, p_0(18) -> 14
, p_0(20) -> 14
, p_0(20) -> 19
, p_0(25) -> 24
, p_1(31) -> 30
, p_1(32) -> 31
, p_1(33) -> 30
, p_1(36) -> 35
, p_1(38) -> 35
, p_1(38) -> 37
, p_1(38) -> 45
, p_1(43) -> 42
, p_1(46) -> 45
, p_1(47) -> 46
, p_1(48) -> 14
, p_1(48) -> 30
, p_1(48) -> 34
, p_1(50) -> 14
, p_1(50) -> 30
, p_1(50) -> 34
, p_1(50) -> 49
, b_0(27) -> 24
, b_0(27) -> 26
, b_1(45) -> 42
, b_1(45) -> 44
, c_0(15) -> 14
, c_1(35) -> 30
, c_1(35) -> 34
, p^#_0(2) -> 8
, p^#_0(11) -> 10
, p^#_1(31) -> 39
, b^#_0(2) -> 9
, c_1_0(10) -> 9
, c_1_1(39) -> 9
, c_4_0() -> 8
, c_4_0() -> 10
, c_4_1() -> 39}
3) { b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, p^#(p(s(x1))) -> c_3(p^#(x1))}
The usable rules for this path are the following:
{ c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, p^#(p(s(x1))) -> c_3(p^#(x1))}
Details:
We apply the weight gap principle, strictly orienting the rules
{c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [1]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [1] x1 + [1]
c_1(x1) = [1] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
and weakly orienting the rules
{c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [1]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [8]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [1] x1 + [1]
c_1(x1) = [1] x1 + [1]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))}
and weakly orienting the rules
{ a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [2]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [8]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [1] x1 + [9]
c_1(x1) = [1] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
and weakly orienting the rules
{ b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [3]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [11]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
b^#(x1) = [1] x1 + [15]
c_1(x1) = [1] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [8]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p^#(p(s(x1))) -> c_3(p^#(x1))}
and weakly orienting the rules
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p^#(p(s(x1))) -> c_3(p^#(x1))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [6]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [10]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [1] x1 + [15]
c_1(x1) = [1] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))}
Weak Rules:
{ p^#(p(s(x1))) -> c_3(p^#(x1))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))}
Weak Rules:
{ p^#(p(s(x1))) -> c_3(p^#(x1))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
Details:
The problem is Match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ a_0(15) -> 14
, a_0(15) -> 20
, a_0(15) -> 22
, a_1(36) -> 14
, a_1(36) -> 31
, a_1(36) -> 35
, a_1(36) -> 50
, a_1(36) -> 52
, s_0(2) -> 2
, s_0(2) -> 15
, s_0(2) -> 17
, s_0(2) -> 28
, s_0(2) -> 36
, s_0(2) -> 38
, s_0(2) -> 46
, s_0(13) -> 12
, s_0(14) -> 11
, s_0(14) -> 13
, s_0(17) -> 16
, s_0(20) -> 19
, s_0(22) -> 21
, s_0(23) -> 14
, s_0(23) -> 20
, s_0(23) -> 22
, s_0(24) -> 23
, s_0(25) -> 24
, s_0(27) -> 26
, s_1(2) -> 39
, s_1(2) -> 47
, s_1(29) -> 25
, s_1(29) -> 27
, s_1(29) -> 43
, s_1(29) -> 45
, s_1(30) -> 29
, s_1(31) -> 30
, s_1(34) -> 33
, s_1(35) -> 32
, s_1(35) -> 34
, s_1(38) -> 37
, s_1(39) -> 48
, s_1(41) -> 14
, s_1(41) -> 20
, s_1(41) -> 22
, s_1(41) -> 31
, s_1(41) -> 35
, s_1(41) -> 50
, s_1(41) -> 52
, s_1(42) -> 41
, s_1(43) -> 42
, s_1(45) -> 44
, s_1(50) -> 49
, s_1(52) -> 51
, p_0(2) -> 15
, p_0(2) -> 17
, p_0(2) -> 28
, p_0(12) -> 11
, p_0(16) -> 15
, p_0(17) -> 28
, p_0(19) -> 14
, p_0(21) -> 14
, p_0(21) -> 20
, p_0(26) -> 25
, p_1(32) -> 31
, p_1(33) -> 32
, p_1(34) -> 31
, p_1(37) -> 36
, p_1(39) -> 36
, p_1(39) -> 38
, p_1(39) -> 46
, p_1(44) -> 43
, p_1(47) -> 46
, p_1(48) -> 47
, p_1(49) -> 14
, p_1(49) -> 31
, p_1(49) -> 35
, p_1(51) -> 14
, p_1(51) -> 31
, p_1(51) -> 35
, p_1(51) -> 50
, b_0(28) -> 25
, b_0(28) -> 27
, b_1(46) -> 43
, b_1(46) -> 45
, c_0(15) -> 14
, c_1(36) -> 31
, c_1(36) -> 35
, p^#_0(2) -> 8
, p^#_0(11) -> 10
, p^#_0(13) -> 18
, p^#_1(32) -> 40
, p^#_1(34) -> 53
, b^#_0(2) -> 9
, c_1_0(10) -> 9
, c_1_1(40) -> 9
, c_3_0(18) -> 10
, c_3_1(53) -> 40}
4) { c^#(s(x1)) -> c_2(p^#(s(p(s(a(p(s(p(s(x1))))))))))
, p^#(s(x1)) -> c_4()}
The usable rules for this path are the following:
{ a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, c^#(s(x1)) -> c_2(p^#(s(p(s(a(p(s(p(s(x1))))))))))
, p^#(s(x1)) -> c_4()}
Details:
We apply the weight gap principle, strictly orienting the rules
{a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [1]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c^#(x1) = [1] x1 + [1]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, p^#(s(x1)) -> c_4()}
and weakly orienting the rules
{a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, p^#(s(x1)) -> c_4()}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [8]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [0]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [4]
b^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c^#(x1) = [1] x1 + [1]
c_2(x1) = [1] x1 + [1]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{c^#(s(x1)) -> c_2(p^#(s(p(s(a(p(s(p(s(x1))))))))))}
and weakly orienting the rules
{ b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, p^#(s(x1)) -> c_4()
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{c^#(s(x1)) -> c_2(p^#(s(p(s(a(p(s(p(s(x1))))))))))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [8]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [8]
c(x1) = [1] x1 + [1]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c^#(x1) = [1] x1 + [9]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
and weakly orienting the rules
{ c^#(s(x1)) -> c_2(p^#(s(p(s(a(p(s(p(s(x1))))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, p^#(s(x1)) -> c_4()
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [12]
s(x1) = [1] x1 + [1]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [6]
c(x1) = [1] x1 + [0]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c^#(x1) = [1] x1 + [15]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, c^#(s(x1)) -> c_2(p^#(s(p(s(a(p(s(p(s(x1))))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, p^#(s(x1)) -> c_4()
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, c^#(s(x1)) -> c_2(p^#(s(p(s(a(p(s(p(s(x1))))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, p^#(s(x1)) -> c_4()
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
Details:
The problem is Match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ a_0(17) -> 14
, a_0(17) -> 16
, a_1(37) -> 28
, a_1(37) -> 32
, a_1(37) -> 34
, a_1(37) -> 36
, a_1(37) -> 44
, a_1(37) -> 48
, s_0(2) -> 2
, s_0(2) -> 17
, s_0(2) -> 19
, s_0(2) -> 25
, s_0(2) -> 37
, s_0(2) -> 39
, s_0(2) -> 54
, s_0(14) -> 13
, s_0(16) -> 15
, s_0(19) -> 18
, s_0(20) -> 14
, s_0(20) -> 16
, s_0(21) -> 20
, s_0(22) -> 21
, s_0(24) -> 23
, s_0(26) -> 22
, s_0(26) -> 24
, s_0(27) -> 26
, s_0(28) -> 27
, s_0(31) -> 30
, s_0(32) -> 29
, s_0(32) -> 31
, s_1(2) -> 40
, s_1(2) -> 55
, s_1(34) -> 33
, s_1(36) -> 35
, s_1(39) -> 38
, s_1(40) -> 56
, s_1(42) -> 22
, s_1(42) -> 24
, s_1(42) -> 51
, s_1(42) -> 53
, s_1(43) -> 42
, s_1(44) -> 43
, s_1(47) -> 46
, s_1(48) -> 45
, s_1(48) -> 47
, s_1(49) -> 14
, s_1(49) -> 16
, s_1(49) -> 28
, s_1(49) -> 32
, s_1(49) -> 34
, s_1(49) -> 36
, s_1(49) -> 44
, s_1(49) -> 48
, s_1(50) -> 49
, s_1(51) -> 50
, s_1(53) -> 52
, p_0(2) -> 17
, p_0(2) -> 19
, p_0(2) -> 25
, p_0(15) -> 14
, p_0(18) -> 17
, p_0(19) -> 25
, p_0(23) -> 22
, p_0(29) -> 28
, p_0(30) -> 29
, p_0(31) -> 28
, p_1(33) -> 28
, p_1(33) -> 32
, p_1(33) -> 44
, p_1(33) -> 48
, p_1(35) -> 28
, p_1(35) -> 32
, p_1(35) -> 34
, p_1(35) -> 44
, p_1(35) -> 48
, p_1(38) -> 37
, p_1(40) -> 37
, p_1(40) -> 39
, p_1(40) -> 54
, p_1(45) -> 44
, p_1(46) -> 45
, p_1(47) -> 44
, p_1(52) -> 51
, p_1(55) -> 54
, p_1(56) -> 55
, b_0(25) -> 22
, b_0(25) -> 24
, b_1(54) -> 51
, b_1(54) -> 53
, c_0(17) -> 28
, c_0(17) -> 32
, c_1(37) -> 44
, c_1(37) -> 48
, p^#_0(2) -> 8
, p^#_0(13) -> 12
, p^#_1(33) -> 41
, c^#_0(2) -> 11
, c_2_0(12) -> 11
, c_2_1(41) -> 11
, c_4_0() -> 8
, c_4_0() -> 12
, c_4_1() -> 41}
5) {b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))}
The usable rules for this path are the following:
{ c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [1]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [1] x1 + [1]
c_1(x1) = [1] x1 + [8]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
and weakly orienting the rules
{c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [1]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [8]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [1] x1 + [1]
c_1(x1) = [1] x1 + [1]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))}
and weakly orienting the rules
{ a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [7]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [8]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [1] x1 + [9]
c_1(x1) = [1] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
and weakly orienting the rules
{ b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [3]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [8]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [2]
b^#(x1) = [1] x1 + [13]
c_1(x1) = [1] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, b^#(s(x1)) -> c_1(p^#(p(s(s(c(p(s(p(s(x1))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
Details:
The problem is Match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ a_0(15) -> 14
, a_0(15) -> 19
, a_0(15) -> 21
, a_1(35) -> 14
, a_1(35) -> 30
, a_1(35) -> 34
, a_1(35) -> 49
, a_1(35) -> 51
, s_0(2) -> 2
, s_0(2) -> 15
, s_0(2) -> 17
, s_0(2) -> 27
, s_0(2) -> 35
, s_0(2) -> 37
, s_0(2) -> 45
, s_0(13) -> 12
, s_0(14) -> 11
, s_0(14) -> 13
, s_0(17) -> 16
, s_0(19) -> 18
, s_0(21) -> 20
, s_0(22) -> 14
, s_0(22) -> 19
, s_0(22) -> 21
, s_0(23) -> 22
, s_0(24) -> 23
, s_0(26) -> 25
, s_1(2) -> 38
, s_1(2) -> 46
, s_1(28) -> 24
, s_1(28) -> 26
, s_1(28) -> 42
, s_1(28) -> 44
, s_1(29) -> 28
, s_1(30) -> 29
, s_1(33) -> 32
, s_1(34) -> 31
, s_1(34) -> 33
, s_1(37) -> 36
, s_1(38) -> 47
, s_1(40) -> 14
, s_1(40) -> 19
, s_1(40) -> 21
, s_1(40) -> 30
, s_1(40) -> 34
, s_1(40) -> 49
, s_1(40) -> 51
, s_1(41) -> 40
, s_1(42) -> 41
, s_1(44) -> 43
, s_1(49) -> 48
, s_1(51) -> 50
, p_0(2) -> 15
, p_0(2) -> 17
, p_0(2) -> 27
, p_0(12) -> 11
, p_0(16) -> 15
, p_0(17) -> 27
, p_0(18) -> 14
, p_0(20) -> 14
, p_0(20) -> 19
, p_0(25) -> 24
, p_1(31) -> 30
, p_1(32) -> 31
, p_1(33) -> 30
, p_1(36) -> 35
, p_1(38) -> 35
, p_1(38) -> 37
, p_1(38) -> 45
, p_1(43) -> 42
, p_1(46) -> 45
, p_1(47) -> 46
, p_1(48) -> 14
, p_1(48) -> 30
, p_1(48) -> 34
, p_1(50) -> 14
, p_1(50) -> 30
, p_1(50) -> 34
, p_1(50) -> 49
, b_0(27) -> 24
, b_0(27) -> 26
, b_1(45) -> 42
, b_1(45) -> 44
, c_0(15) -> 14
, c_1(35) -> 30
, c_1(35) -> 34
, p^#_0(2) -> 8
, p^#_0(11) -> 10
, p^#_1(31) -> 39
, b^#_0(2) -> 9
, c_1_0(10) -> 9
, c_1_1(39) -> 9}
6) {c^#(s(x1)) -> c_2(p^#(s(p(s(a(p(s(p(s(x1))))))))))}
The usable rules for this path are the following:
{ a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, c^#(s(x1)) -> c_2(p^#(s(p(s(a(p(s(p(s(x1))))))))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [1]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [2]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c^#(x1) = [1] x1 + [1]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{c^#(s(x1)) -> c_2(p^#(s(p(s(a(p(s(p(s(x1))))))))))}
and weakly orienting the rules
{ a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{c^#(s(x1)) -> c_2(p^#(s(p(s(a(p(s(p(s(x1))))))))))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [7]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [8]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c^#(x1) = [1] x1 + [9]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
and weakly orienting the rules
{ c^#(s(x1)) -> c_2(p^#(s(p(s(a(p(s(p(s(x1))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [3]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [12]
a^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c^#(x1) = [1] x1 + [9]
c_2(x1) = [1] x1 + [1]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, c^#(s(x1)) -> c_2(p^#(s(p(s(a(p(s(p(s(x1))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, c^#(s(x1)) -> c_2(p^#(s(p(s(a(p(s(p(s(x1))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
Details:
The problem is Match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ a_0(17) -> 14
, a_0(17) -> 16
, a_1(33) -> 28
, a_1(33) -> 32
, a_1(33) -> 39
, a_1(33) -> 41
, s_0(2) -> 2
, s_0(2) -> 17
, s_0(2) -> 19
, s_0(2) -> 25
, s_0(2) -> 33
, s_0(2) -> 35
, s_0(2) -> 47
, s_0(14) -> 13
, s_0(16) -> 15
, s_0(19) -> 18
, s_0(20) -> 14
, s_0(20) -> 16
, s_0(21) -> 20
, s_0(22) -> 21
, s_0(24) -> 23
, s_1(2) -> 36
, s_1(2) -> 48
, s_1(26) -> 22
, s_1(26) -> 24
, s_1(26) -> 44
, s_1(26) -> 46
, s_1(27) -> 26
, s_1(28) -> 27
, s_1(31) -> 30
, s_1(32) -> 29
, s_1(32) -> 31
, s_1(35) -> 34
, s_1(36) -> 49
, s_1(39) -> 38
, s_1(41) -> 40
, s_1(42) -> 14
, s_1(42) -> 16
, s_1(42) -> 28
, s_1(42) -> 32
, s_1(42) -> 39
, s_1(42) -> 41
, s_1(43) -> 42
, s_1(44) -> 43
, s_1(46) -> 45
, p_0(2) -> 17
, p_0(2) -> 19
, p_0(2) -> 25
, p_0(15) -> 14
, p_0(18) -> 17
, p_0(19) -> 25
, p_0(23) -> 22
, p_1(29) -> 28
, p_1(30) -> 29
, p_1(31) -> 28
, p_1(34) -> 33
, p_1(36) -> 33
, p_1(36) -> 35
, p_1(36) -> 47
, p_1(38) -> 28
, p_1(38) -> 32
, p_1(40) -> 28
, p_1(40) -> 32
, p_1(40) -> 39
, p_1(45) -> 44
, p_1(48) -> 47
, p_1(49) -> 48
, b_0(25) -> 22
, b_0(25) -> 24
, b_1(47) -> 44
, b_1(47) -> 46
, c_1(33) -> 28
, c_1(33) -> 32
, p^#_0(2) -> 8
, p^#_0(13) -> 12
, p^#_1(38) -> 37
, c^#_0(2) -> 11
, c_2_0(12) -> 11
, c_2_1(37) -> 11}
7) { a^#(s(x1)) -> c_0(p^#(s(b(p(p(s(s(x1))))))))
, p^#(s(x1)) -> c_4()}
The usable rules for this path are the following:
{ b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, a^#(s(x1)) -> c_0(p^#(s(b(p(p(s(s(x1))))))))
, p^#(s(x1)) -> c_4()}
Details:
We apply the weight gap principle, strictly orienting the rules
{ b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, p^#(s(x1)) -> c_4()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, p^#(s(x1)) -> c_4()}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [8]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [0]
a^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [0]
p^#(x1) = [1] x1 + [2]
b^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{a^#(s(x1)) -> c_0(p^#(s(b(p(p(s(s(x1))))))))}
and weakly orienting the rules
{ b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, p^#(s(x1)) -> c_4()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{a^#(s(x1)) -> c_0(p^#(s(b(p(p(s(s(x1))))))))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [8]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [3]
c(x1) = [1] x1 + [1]
a^#(x1) = [1] x1 + [9]
c_0(x1) = [1] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
and weakly orienting the rules
{ a^#(s(x1)) -> c_0(p^#(s(b(p(p(s(s(x1))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, p^#(s(x1)) -> c_4()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [14]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [6]
c(x1) = [1] x1 + [0]
a^#(x1) = [1] x1 + [12]
c_0(x1) = [1] x1 + [1]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, a^#(s(x1)) -> c_0(p^#(s(b(p(p(s(s(x1))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, p^#(s(x1)) -> c_4()}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, a^#(s(x1)) -> c_0(p^#(s(b(p(p(s(s(x1))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, p^#(s(x1)) -> c_4()}
Details:
The problem is Match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ a_1(27) -> 16
, a_1(27) -> 20
, a_1(27) -> 24
, a_1(27) -> 26
, a_1(27) -> 39
, a_1(27) -> 43
, s_0(2) -> 2
, s_0(2) -> 12
, s_0(2) -> 13
, s_0(2) -> 21
, s_0(2) -> 27
, s_0(2) -> 29
, s_0(2) -> 34
, s_0(11) -> 10
, s_0(13) -> 22
, s_0(14) -> 11
, s_0(15) -> 14
, s_0(16) -> 15
, s_0(19) -> 18
, s_0(20) -> 17
, s_0(20) -> 19
, s_1(2) -> 30
, s_1(2) -> 35
, s_1(24) -> 23
, s_1(26) -> 25
, s_1(29) -> 28
, s_1(30) -> 36
, s_1(33) -> 32
, s_1(37) -> 11
, s_1(37) -> 33
, s_1(37) -> 46
, s_1(38) -> 37
, s_1(39) -> 38
, s_1(42) -> 41
, s_1(43) -> 40
, s_1(43) -> 42
, s_1(44) -> 16
, s_1(44) -> 20
, s_1(44) -> 24
, s_1(44) -> 26
, s_1(44) -> 39
, s_1(44) -> 43
, s_1(45) -> 44
, s_1(46) -> 45
, p_0(2) -> 12
, p_0(2) -> 13
, p_0(2) -> 21
, p_0(13) -> 12
, p_0(17) -> 16
, p_0(18) -> 17
, p_0(19) -> 16
, p_0(22) -> 21
, p_1(23) -> 16
, p_1(23) -> 20
, p_1(23) -> 39
, p_1(23) -> 43
, p_1(25) -> 16
, p_1(25) -> 20
, p_1(25) -> 24
, p_1(25) -> 39
, p_1(25) -> 43
, p_1(28) -> 27
, p_1(30) -> 27
, p_1(30) -> 29
, p_1(30) -> 34
, p_1(32) -> 46
, p_1(35) -> 34
, p_1(36) -> 35
, p_1(40) -> 39
, p_1(41) -> 40
, p_1(42) -> 39
, b_0(12) -> 11
, b_1(34) -> 33
, b_1(34) -> 46
, c_0(21) -> 16
, c_0(21) -> 20
, c_1(27) -> 39
, c_1(27) -> 43
, a^#_0(2) -> 6
, c_0_0(9) -> 6
, c_0_1(31) -> 6
, p^#_0(2) -> 8
, p^#_0(10) -> 9
, p^#_1(32) -> 31
, c_4_0() -> 8
, c_4_0() -> 9
, c_4_1() -> 31}
8) {a^#(s(x1)) -> c_0(p^#(s(b(p(p(s(s(x1))))))))}
The usable rules for this path are the following:
{ b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, a^#(s(x1)) -> c_0(p^#(s(b(p(p(s(s(x1))))))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, a^#(s(x1)) -> c_0(p^#(s(b(p(p(s(s(x1))))))))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, a^#(s(x1)) -> c_0(p^#(s(b(p(p(s(s(x1))))))))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [0]
a^#(x1) = [1] x1 + [9]
c_0(x1) = [1] x1 + [0]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
and weakly orienting the rules
{ b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, a^#(s(x1)) -> c_0(p^#(s(b(p(p(s(s(x1))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [8]
c(x1) = [1] x1 + [1]
a^#(x1) = [1] x1 + [9]
c_0(x1) = [1] x1 + [1]
p^#(x1) = [1] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
and weakly orienting the rules
{ c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, a^#(s(x1)) -> c_0(p^#(s(b(p(p(s(s(x1))))))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
Details:
Interpretation Functions:
a(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [10]
c(x1) = [1] x1 + [6]
a^#(x1) = [1] x1 + [15]
c_0(x1) = [1] x1 + [1]
p^#(x1) = [1] x1 + [2]
b^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, a^#(s(x1)) -> c_0(p^#(s(b(p(p(s(s(x1))))))))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))}
Weak Rules:
{ p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, a^#(s(x1)) -> c_0(p^#(s(b(p(p(s(s(x1))))))))}
Details:
The problem is Match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ a_0(21) -> 16
, a_0(21) -> 20
, a_0(21) -> 24
, a_1(38) -> 16
, a_1(38) -> 20
, a_1(38) -> 35
, a_1(38) -> 37
, a_1(38) -> 42
, a_1(38) -> 46
, s_0(2) -> 2
, s_0(2) -> 12
, s_0(2) -> 13
, s_0(2) -> 21
, s_0(2) -> 30
, s_0(2) -> 38
, s_0(11) -> 10
, s_0(13) -> 22
, s_0(14) -> 11
, s_0(15) -> 14
, s_0(16) -> 15
, s_0(19) -> 18
, s_0(20) -> 17
, s_0(20) -> 19
, s_0(24) -> 23
, s_1(2) -> 31
, s_1(2) -> 33
, s_1(25) -> 16
, s_1(25) -> 20
, s_1(25) -> 24
, s_1(25) -> 35
, s_1(25) -> 37
, s_1(25) -> 42
, s_1(25) -> 46
, s_1(26) -> 25
, s_1(27) -> 26
, s_1(29) -> 28
, s_1(30) -> 39
, s_1(33) -> 32
, s_1(35) -> 34
, s_1(37) -> 36
, s_1(40) -> 11
, s_1(40) -> 27
, s_1(40) -> 29
, s_1(41) -> 40
, s_1(42) -> 41
, s_1(45) -> 44
, s_1(46) -> 43
, s_1(46) -> 45
, p_0(2) -> 12
, p_0(2) -> 13
, p_0(2) -> 21
, p_0(13) -> 12
, p_0(17) -> 16
, p_0(18) -> 17
, p_0(19) -> 16
, p_0(19) -> 20
, p_0(22) -> 21
, p_0(23) -> 16
, p_0(23) -> 20
, p_1(28) -> 27
, p_1(31) -> 30
, p_1(31) -> 38
, p_1(32) -> 31
, p_1(33) -> 30
, p_1(33) -> 38
, p_1(34) -> 16
, p_1(34) -> 20
, p_1(34) -> 42
, p_1(34) -> 46
, p_1(36) -> 16
, p_1(36) -> 20
, p_1(36) -> 35
, p_1(36) -> 42
, p_1(36) -> 46
, p_1(39) -> 38
, p_1(41) -> 42
, p_1(41) -> 46
, p_1(43) -> 42
, p_1(43) -> 46
, p_1(44) -> 43
, p_1(45) -> 42
, p_1(45) -> 46
, b_0(12) -> 11
, b_1(30) -> 27
, b_1(30) -> 29
, c_0(21) -> 16
, c_0(21) -> 20
, c_1(38) -> 42
, c_1(38) -> 46
, a^#_0(2) -> 6
, c_0_0(9) -> 6
, c_0_1(47) -> 6
, p^#_0(2) -> 8
, p^#_0(10) -> 9
, p^#_1(28) -> 47}